Design verification systems perform the task of verifying that a given hardware design satisfies its specified requirements. Design verification is typically performed by a verification tool, which subjects the tested design to various test cases and scenarios. Various known verification methods can be used for this purpose, such as simulation-based methods and/or formal verification methods.
The verification process is sometimes carried out using a methodology referred to as Assertion-based Verification (ABV). In ABV, properties of the design are formulated as directives to the verification tool, such as assertions. Several standardized assertion languages are used for specifying assertions, such as the Property Specification Language (PSL) and the SystemVerilog® Assertions (SVA) language. PSL is specified in “Standard for Property Specification Language (PSL),” IEEE standard 1850-2007, 2007, also known as IEC 62531:2007(E). SVA is specified in “IEEE Standard for SystemVerilog—Unified Hardware Design, Specification and Verification Language,” IEEE Standard 1800-2005, 2005.
Verification directives may include local variables that are used for tracking information during different stages of the verification process. Methods for processing assertions that include local variables are described, for example, by Bustan and Havlicek in “Some Complexity Results for SystemVerilog Assertions,” Proceedings of the 18th International Conference on Computer Aided Verification (CAV), Seattle, Wash., Aug. 17-20, 2006, pages 205-218, and by Long and Seawright in “Synthesizing SVA Local Variables for Formal Verification,” Proceedings of the 44th ACM/IEEE Design Automation Conference (DAC), San Diego, Calif., Jun. 4-8, 2007, pages 75-80.
Design properties are sometimes represented by finite automata, or state machines. Automata-based methods are described, for example, by Ben-David et al., in “Automata Construction for On-The-Fly Model Checking PSL Safety Simple Subset,” IBM Research Report H-0258, June, 2005, and in “The Safety Simple Subset,” Proceedings of the Haifa Verification Conference, Haifa, Israel, Nov. 13-16, 2005, pages 14-29.
As another example, U.S. Pat. No. 7,188,061 describes a method for design verification, which includes receiving a software model of a design of a system under evaluation, and providing a property, which is dependent on a specified variable having a predefined range of values. The property applies to all states of the system for any selected value among the values of the variable within the predefined range. The property is processed so as to generate a checker program for detecting a violation of the property. A simulation of the system is then run using the software model together with the checker program.